\begin{tabbing}
$\forall$${\it es}$:ES, ${\it Cmd}$:Type, ${\it In}$:AbsInterface(${\it Cmd}$), ${\it Sys}$:AbsInterface(Top).
\\[0ex](E(${\it In}$) $\subseteq$r E(${\it Sys}$))
\\[0ex]$\Rightarrow$ \=($\forall$$f$:sys{-}antecedent(${\it es}$;${\it Sys}$).\+
\\[0ex]($\forall$$u$:E(${\it Sys}$). ($f$($u$) = $u$ $\in$ E) $\Rightarrow$ ($\uparrow$($u$ $\in_{b}$ ${\it In}$)))
\\[0ex]$\Rightarrow$ ($\forall$$e$:E(${\it Sys}$). cr{-}explanation\{i:l\}(${\it es}$; ${\it Sys}$; $f$; $e$) $\in$ (E(${\it In}$) List)))
\-
\end{tabbing}